//
// Created by yy N on 2022/4/15.
//

#ifndef SATENCODINGFORPATHPLANNING_PROBLEM_H
#define SATENCODINGFORPATHPLANNING_PROBLEM_H

#include <vector>
#include <list>
enum states{
    EMPTY = 0,
    BLOCKED = 1,
    WALKER = 2
};
enum actions{
    UP = 0,
    DOWN = 1,
    LEFT = 2,
    RIGHT = 3
};
class Problem {
    int row;
    int col;
    int step;
    int numOfStateVariables;
    int numOfActionVariables;
    int numOfVariables;
    std::vector< std::vector<bool>> * pmatrix;
    std::vector< bool> *pres;
    std::list<std::vector<int>> clauses;

public:
    Problem(int r, int c, int s);

    virtual ~Problem();

    void printInfo();

    void showMatrix(int x, int y) const;

    void resetStep(int s);

    // 返回状态变量编号
    // 参数 i j：位置信息 t：时间 s：状态
    int stateIndex(int i, int j, int t, int s) const{
        if(i >= 0 && i <= row-1 && j >= 0 && j <= col-1 && t >= 0 && t <= step){
            return (row * col * 3 * t) + (row * col * s) + (i * row + j + 1);
        }
        else{
            std::cerr << "stateIndex: i " << i << " j " << j <<" t " << t << " out of range!";
            exit(-1);
        }
    }

    // 返回动作变量编号
    int actionIndex(int i, int j, int t, int a) const{
        if(i >= 0 && i <= row-1 && j >= 0 && j <= col-1 && t >= 0 &&t <= step-1)
        {
            return numOfStateVariables + (row * col * 4 * t) + (row * col * a) + i * row + j + 1;
        }else{
            std::cerr << "actionIndex: i " << i << " j " << j <<" t " << t << " out of range!";
            exit(-1);
        }
    }

    //addClause(std::vector<int>{});
    inline void addClause(const std::vector<int> &c){
        clauses.push_back(c);
    }

    void initMatrix();

    // 处理过程
    // 根据地图初始化变量， 设定起始条件和目标条件
    // The first state is the initial state
    // The goal conditions are satisfied in the end
    void initial();

    // 状态变量的唯一性
    // Each state variable has at least one value
    // Each state variable has at most one value
    void uniquenessOfState(int i, int j, int t);

    // 动作变量的前置条件与后置条件
    // If an action is applied it must be applicable
    // If an action is applied its effects are applied in the next step
    void actionConditions(int i, int j, int t);

    // 状态变化的必要条件
    // State variables cannot change without an action between steps
    void nessConditionOfStateChanging(int i, int j, int t);

    // 每一步动作的唯一性
    // At most one action is used in each step
    void uniquenessOfAction(int i, int j, int t);

    // clause 生成过程
    void genClauses();

    // 存储 CNF 格式的 encoding 结果
    void saveCNF(const std::string& filename);

    // 可视化查看移动过程
    void parseResult();

    // 调用 z3 并解析结果, sat返回 true， unsat返回 false
    bool getResult();

    // 展示每一步各个变量的状态，发生bug调试用
    void showMoving(std::vector<bool> &res) const;

};


#endif //SATENCODINGFORPATHPLANNING_PROBLEM_H
